…I gate (#79)

## Summary
The Lean 4 formal-verification file
`docs/proofs/verification/WokeLang.lean` claimed *"all 12 `sorry`
eliminated / verified"* — but it had **silently bit-rotted** and did
**not compile** under a current Lean toolchain (~100 errors). Root
cause: **no CI ever ran the prover** (workflows only covered the OCaml
core + e2e), so the headline correctness claim was never
machine-enforced.

This PR restores **sorry-free compilation under Lean 4.30.0**, adds the
missing **CI gate**, and documents a coverage/correspondence audit.

## What changed
**Only proof bodies + 2 `deriving` clauses + 1 `abbrev`** — every
theorem signature and every inductive is **byte-identical** (verified by
diff). No statement was weakened; no `sorry`/`admit`/`axiom` introduced.

Root causes fixed:
- **`DecidableEq` no longer derives** for `Value`/`WokeType` (`Float`
has none — NaN; and nested `List Self` blocks the deriving handler) →
reduced to `deriving Repr`; equality decisions use Lean's classical
`by_cases` (no instance needed).
- **`induction`/`cases` on concrete indices** (`emptyTypeEnv`,
`emptyEnv`) + binder-arity drift across Lean versions. `preservation`
made **type-polymorphic** via `induction hs generalizing t` (its
congruence cases need the IH at the operand type, not the result type).
`cases … with | inr ⟨..⟩` anonymous-constructor patterns → `obtain` (no
longer supported in `cases`). Type-mismatched reduction siblings
discharged with `nomatch`.
- **`BEq Permission`**: made `Permission` a reducible `abbrev` so the
`String` instance transfers.

## Verification
```
$ lean docs/proofs/verification/WokeLang.lean   # exit 0, no output
```
Machine-checked: `progress`, `preservation`, `type_safety` (multi-step),
`consent_monotonicity`, `consent_preservation` — for the expression core
(incl. the Result/`unwrap`/`error` panic-propagation fragment).

## Added
- **`docs/proofs/verification/lean-toolchain`** — pins Lean v4.30.0.
- **`docs/proofs/verification/AUDIT.md`** — answers PROOF-NEEDS.md #1 &
#2: the proofs cover a **clean expression core** (a strict,
honestly-scoped subset), the Lean type system corresponds to the
**Rust** typechecker (not the OCaml `core/eval.ml`, which models a
different language), and the consent theorems correspond to the spec's
Hoare logic.
- **`.github/workflows/lean-proofs.yml`** — installs the pinned
toolchain and runs the check on every push to the proof dir, so this
can't bit-rot again. SHA-pinned action, pure-bash install (matches
estate governance).

## Note on scope
This repairs and re-verifies the **existing** proofs and makes them
durable. It does **not** yet extend coverage (more binops/comparisons,
statements, arrays, compiler/VM correctness) — those remain per
PROOF-NEEDS.md and are tabulated in AUDIT.md.

https://claude.ai/code/session_013wg3Mtq2QFhYi4XVw1Z6z7

---
_Generated by [Claude
Code](https://claude.ai/code/session_013wg3Mtq2QFhYi4XVw1Z6z7)_

Co-authored-by: Claude <noreply@anthropic.com>

…ation state (#83)

## Why

The Lean + Coq proof repair/extension landed in **#79–#82 (all merged)**
but was **invisible to the estate's bot-coordination layer**. The
machine-readable state still described a pre-proof-work world:

- `STATE.a2ml [frontier]` named only an aspirational Isabelle narrative
and **omitted the existing, now-verified Lean+Coq type-safety track**
entirely; `last-shepherd` stopped at #77.
- `debt.a2ml` carried **zero** real items — so the documented proof
follow-ups would not reach the next session's Phase 0.
- `coverage.a2ml` had no record that `docs/proofs/verification/` was
visited.
- `methodology.a2ml`'s divergent-mode invariants were generic template
stubs — one example literally read *"Idris2 only … no Lean4, Coq"*, the
**opposite** of reality, a real footgun for a divergent-mode bot.

## What (all additive; no curated content overwritten)

Surfaced through the channels whose own contracts say *"updated by
agents at session end"*:

| File | Change |
|---|---|
| `bot_directives/debt.a2ml` | Carry-forward follow-ups as Phase-0
input: **should** — Coq binop parity, Lean array typing (Coq's is a
ready template), `cap_subsumes_trans`; **could** — Coq `preservation`
clean rewrite, Lean float binops, echo-types L3 integration blueprint. |
| `bot_directives/coverage.a2ml` | `docs/proofs/verification/` recorded
as a visited component (PRs #79–#82). |
| `bot_directives/methodology.a2ml` | `divergent-invariants`: provers
are **Lean 4 + Coq** (not Idris2/Isabelle); admit/sorry stay **zero**;
the `Coq.Reals` axioms are **permitted, not escape hatches** (don't let
an Axiom-scanner flag them). `known-constraints`: CI-gated +
toolchain-pinned (Coq is version-sensitive); Lean/Coq cover
**complementary** subsets; PROOF-NEEDS #2 is **ill-posed** pending a
maintainer (a)/(b) decision. |
| `6a2/STATE.a2ml` | Added `type-safety-proofs` to `[frontier]`; added
`proof-gates` + `last-proof-shepherd` to `[ci]`. Existing lines
preserved. |

Source of truth for every claim:
[`docs/proofs/verification/AUDIT.md`](../blob/main/docs/proofs/verification/AUDIT.md).

## Notes for review

- **Draft on purpose** — `.machine_readable/` is maintainer-curated
(`gitbot-fleet`/`hypatia` are both barred from it), so this goes through
human review rather than direct-to-`main`.
- The only deletions are replaced **generic template-example comments**
in `methodology.a2ml` (incl. the misleading "Idris2 only" stub). No real
data removed.
- `coverage.a2ml`'s `total/visited` summary counters were left untouched
— I won't fabricate a component denominator.
- Stacked on the merged #82; the net diff is the four files above.

https://claude.ai/code/session_013wg3Mtq2QFhYi4XVw1Z6z7

---
_Generated by [Claude
Code](https://claude.ai/code/session_013wg3Mtq2QFhYi4XVw1Z6z7)_

---------

Co-authored-by: Claude <noreply@anthropic.com>